\begin{tabbing}
$\forall$${\it poss}$:(ES\{i\}$\rightarrow$Prop$_{\mbox{\scriptsize i'}}$), $T$:Type$_{\mbox{\scriptsize i}}$, $s$:$T$, $i$:Id, $P$, $Q$:(possible{-}event\{i:l\}(${\it poss}$)$\rightarrow$Prop$_{\mbox{\scriptsize i'}}$).
\\[0ex]($\forall$$e$:possible{-}event\{i:l\}(${\it poss}$). $P$($e$) $\Rightarrow$ $Q$($e$))
\\[0ex]$\Rightarrow$ (\=$\forall$$R$:(possible{-}event\{i:l\}(${\it poss}$)$\rightarrow$possible{-}event\{i:l\}(${\it poss}$)$\rightarrow$Prop$_{\mbox{\scriptsize i'}}$), ${\it Rs}$:($T$$\rightarrow$$T$$\rightarrow$Prop$_{\mbox{\scriptsize i'}}$).\+
\\[0ex]ma{-}knows\{i:l\}(${\it poss}$; $i$; $T$; $s$; $P$; ${\it Rs}$; $R$) $\Rightarrow$ ma{-}knows\{i:l\}(${\it poss}$; $i$; $T$; $s$; $Q$; ${\it Rs}$; $R$))
\-
\end{tabbing}